Nuprl Lemma : qadd-non-neg
11,40
postcript
pdf
a
,
b
:
. 0
a
0
b
0
a
+
b
latex
Definitions
P
Q
,
P
&
Q
,
T
,
P
Q
,
True
,
,
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
{
T
}
,
S
T
Lemmas
qle
transitivity
qorder
,
mon
ident
q
,
qadd
comm
q
,
true
wf
,
squash
wf
,
qadd
wf
,
rationals
wf
,
int
inc
rationals
,
qle
wf
,
qadd
preserves
qle
origin
a, b:
. 0 
a 
0 b 0 a + b a, b:. 0 a 0 b 0 a + b 
Q
T Q
T Qx:A. B(x)
T